(* Copyright Per Lindgren 2015, see the file "LICENSE" *)
(* for the full license governing this code.           *)

(* FUN-4SURE/ST *)

open Common
open AST
                                     
(* printing in ST *)

let st_of_int i   = string_of_int i
let st_of_id id   = Id.get_s id
let st_of_idl idl = "{" ^ String.concat ", " (List.map st_of_id idl) ^ "}"

let st_of_bo = function
  | true  -> "TRUE"
  | false -> "FALSE" 

let rec st_of_op = function
  | OpMul  -> "*"
  | OpDiv  -> "/"
  | OpMod  -> "MOD"
  | OpAdd  -> "+"
  | OpSub  -> "-"
  | OpEq   -> "=="
  | OpNeq  -> "!="
  | OpGt   -> ">"
  | OpGEq  -> ">="
  | OpLt   -> "<"
  | OpLEq  -> "<="
  | OpAnd  -> "AND"
  | OpOr   -> "OR"
  | OpExor -> "EXOR"
and st_of_uexp = function
  | UNot   -> "NOT"
  | UMinus -> "-"
and st_of_exp = function
  | OpExp (op, e1, e2) -> "(" ^ st_of_exp e1 ^ " " ^ st_of_op op ^ " " ^ st_of_exp e2 ^ ")"
  | IdExp (id)         -> st_of_id id
  | IntExp (i)         -> st_of_int i
  | CharExp (c)        -> ecit ^ String.make 1 c ^ ecit
  | BoolExp (b)        -> st_of_bo b
  | UnOpExp (uop, e)   -> "(" ^ st_of_uexp uop ^ " (" ^ st_of_exp e ^ ") )"

let st_of_st_stmt = function
  | StmtAssign (lval, exp) -> st_of_id lval ^ " := " ^ st_of_exp exp 
  | StmtAssert (exp)       -> "assert { " ^ st_of_exp exp ^ " }"  
  
let st_of_gu_exp exp = 
  "[ " ^ st_of_exp exp ^ " ]"  
        
let st_of_gu = function
  | EcGuard (Some t, _, _)     -> "AFTER " ^ st_of_int t 
  | EcGuard (_, None, exp)     -> st_of_gu_exp exp
  | EcGuard (_, Some evt, exp) -> st_of_id evt ^ " " ^ st_of_gu_exp exp
  
let st_of_tr tl = 
  let tr = function
    | EcTrans (f,t,g) -> "  " ^ st_of_id f ^ " TO " ^ st_of_id t ^ " := " ^ st_of_gu g ^ ";"
    in
    myconcat nl (List.map tr tl)

let st_of_action = function
  | EcAction (Some aid, eidl) -> st_of_id aid ^ " -> " ^ String.concat ", " (List.map st_of_id eidl)
  | EcAction (None, eidl)     -> " -> " ^ String.concat ", " (List.map st_of_id eidl)
    
let st_of_sl sl =
  let st = function
    | EcState (sid, al) -> "  " ^ st_of_id sid ^ " : " ^ String.concat ", " (List.map st_of_action al) ^ ";"
  in   
  myconcat nl (List.map st sl)

let st_of_contract cl = 
  let co = function
    | Requires expr  -> "  requires { " ^ st_of_exp expr ^ " }"       
    | Ensures  expr  -> "  ensures  { " ^ st_of_exp expr ^ " }" 
    | ReqRaw   s     -> "  requires " ^ s       
    | EnsRaw   s     -> "  ensures  " ^ s
  in
  myconcat nl (List.map co cl)
    
let st_of_ecc = function
  | None -> "" (* if no ECC  skip *)
  | Some FbEcc (sl, cl, tl) ->     
    "EC_STATES" ^ nl ^  st_of_contract cl ^ st_of_sl sl ^ "END_STATES" ^ nl ^ 
    "EC_TRANSITIONS" ^ nl ^  st_of_tr tl ^ "END_TRANSITIONS" ^ nl 

let st_of_ptype = function
  | Int  -> "INT"
  | Bool -> "BOOL"
  | Char -> "CHAR"
  | Byte -> "BYTE"
   
let st_of_event id =
  st_of_id id  
  
let st_of_v = function
  | Var (id, t) -> st_of_id id ^ " : " ^ st_of_ptype t 
let st_of_vl vl = String.concat ", " (List.map st_of_v vl)
    
let st_of_e_id e_id = 
  match e_id with | Event (e_id, _, _) -> st_of_id e_id
  
let st_of_e_idl e_idl = String.concat ", " (List.map st_of_e_id e_idl)
        
let st_of_fb_if = function
  | FbIf (ei_idl, eo_idl, vil, vol) ->
   "EVENT_INPUT"  ^ nl ^ "  " ^ st_of_e_idl ei_idl ^ nl ^ "END_EVENT" ^ nl ^ nl ^
   "EVENT_OUTPUT" ^ nl ^ "  " ^ st_of_e_idl eo_idl ^ nl ^ "END_EVENT" ^ nl ^ nl ^ 
  
   "VAR_INPUT"  ^ nl ^ "  " ^ st_of_vl vil ^ nl ^ "END_VAR" ^ nl ^ nl ^
   "VAR_OUTPUT" ^ nl ^ "  " ^ st_of_vl vol ^ nl ^ "END_VAR" ^ nl ^ nl  

let st_of_fb_v = function
  | FbVar vl ->
    "VAR" ^ nl ^ "  " ^ st_of_vl vl ^ nl ^ "END_VAR" ^ nl ^ nl

let st_of_alg = function
  | FbAlg (aid, cont, vo, stmtl) -> 
    "ALGORITHM " ^ st_of_id aid ^ " IN ST " ^ nl ^ 
    st_of_contract cont ^  
    "  : " ^ nl ^ 
    (
      match vo with
      | [] -> ""
      | vl -> "VAR_TEMP " ^ nl ^ st_of_vl vl ^ nl ^ "VAR_END" ^ nl 
    ) ^ 
    myconcat (" ;" ^ nl) (List.map st_of_st_stmt stmtl) ^ 
    "END_ALGORITHM" 
      
let st_of_algs algl = 
  
  myconcat nl (List.map st_of_alg algl)
                         
let st_of_fbs tl = 
  let fb = function
    | FB (fb_id, fb_if, fb_v, ecc, algl) -> 
      "FUNCTION_BLOCK " ^ st_of_id fb_id ^ nl ^ 
      st_of_fb_if fb_if ^
      st_of_fb_v fb_v ^
      st_of_ecc ecc ^ 
      st_of_algs algl ^ 
      "END_FUNCTION_BLOCK"
  in
  myconcat nl (List.map fb tl) 

    
